A *(Learning Lounge) course.

<a href="http://www.diku.dk/forskning/topps/bibliography/1998.html#D-368">Lectures on the Curry-Howard Isomorphism</a> is a nice text which starts out with explaining untyped and typed _(lambda calculus), then constructivistic logic and _(curry-howard isomorphism), combinatory logic and then other related advanced stuff about this.